Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

f(c(c(a, y, a), b(x, z), a)) → b(y, f(c(f(a), z, z)))
f(b(b(x, f(y)), z)) → c(z, x, f(b(b(f(a), y), y)))
c(b(a, a), b(y, z), x) → b(a, b(z, z))

Q is empty.


QTRS
  ↳ DirectTerminationProof

Q restricted rewrite system:
The TRS R consists of the following rules:

f(c(c(a, y, a), b(x, z), a)) → b(y, f(c(f(a), z, z)))
f(b(b(x, f(y)), z)) → c(z, x, f(b(b(f(a), y), y)))
c(b(a, a), b(y, z), x) → b(a, b(z, z))

Q is empty.

We use [23] with the following order to prove termination.

Recursive path order with status [2].
Quasi-Precedence:
[f1, c3] > b2 > a

Status:
a: multiset
c3: [1,2,3]
b2: [2,1]
f1: [1]